<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>Lean community</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  

  <div class="row justify-content-center mt-4">
    <div class="col-md-6 text-center">  
    <img src="img/community_logo_emb.svg" alt="Lean community"
                class="img-fluid w-100"/>
    </div>
  </div>
  <div class="row mt-5">
    <div class="col">
		<h2 id="lean-and-its-mathematical-library" class="markdown-heading">Lean and its Mathematical Library <a class="hover-link" href="#lean-and-its-mathematical-library">#</a></h2>
<p>The <a href="https://leanprover.github.io">Lean theorem prover</a>
is a proof assistant developed principally by Leonardo de Moura at Microsoft Research.</p>
<p>The Lean mathematical library, <em>mathlib</em>, is a community-driven effort
to build a unified library of mathematics formalized in the
Lean proof assistant. The library also contains definitions
useful for programming. This project is very active, with many
regular contributors and daily activity.</p>
<p>The contents, design, and community organization of mathlib are
described in the paper
<a href="https://arxiv.org/abs/1910.09336">The Lean mathematical library</a>, which appeared
at CPP 2020. You can get a bird's eye view of what is in the library by
reading <a href="mathlib-overview.html">the library overview</a>.
You can also have a look at our <a href="mathlib_stats.html">repository statistics</a>
to see how it grows and who contributes to it.</p>

	</div>
  </div>
  <div class="row justify-content-center mt-3">
   <div class="card-deck">
      <div class="card">
        <div class="card-body">
		  <h4>Try it!</h4>
          <p>
          You can 
          try Lean in your web browser, 
          install it in an isolated folder, 
          or go for the full install. 
          Lean is free, open source software. It works on 
          Linux, Windows, and MacOS.
          </p>
		</div>
		<ul class="list-group list-group-flush border-top">
          <li class="list-group-item"><a href="https://leanprover-community.github.io/lean-web-editor"
                 >Try the online version of Lean</a></li>
          <li class="list-group-item"><a href="get_started.html#regular-install"
                 >Installation instructions</a></li>
          <li class="list-group-item"><a href="install/project.html">Working on Lean projects</a></li>
        </ul>
      </div>
      <div class="card">
        <div class="card-body">
		<h4>Learn to Lean!</h4>
		<p>
    You can learn by playing a game, following tutorials, 
    or reading books.
		</p>
		</div>
		<ul class="list-group list-group-flush border-top">
          <li class="list-group-item"><a href="learn.html">Learning resources</a></li>
          <li class="list-group-item"><a href="https://leanprover.github.io/theorem_proving_in_lean/"
                 >Theorem Proving in Lean</a> (an introduction)</li>
          <li class="list-group-item"><a href="https://leanprover-community.github.io/mathlib_docs"
                 >API documentation of mathlib</a></li>
        </ul>
      </div>
      <div class="card">
        <div class="card-body">
		<h4>Meet the community!</h4>
		<p>
        Lean has very diverse and active community. It gathers mostly on
    a <a href="https://leanprover.zulipchat.com/">Zulip chat</a> 
    and on <a href="https://github.com/leanprover-community/mathlib">GitHub</a>. 
    You can get involved and join the fun!
		</p>
		</div>
		<ul class="list-group list-group-flush border-top">
          <li class="list-group-item"><a href="meet.html">Meet us</a></li>
          <li class="list-group-item"><a href="contribute/index.html"
                 >How to contribute</a></li>
          <li class="list-group-item"><a href="papers.html"
                 >Papers involving Lean</a></li>
        </ul>
      </div>
    </div>
  </div>
  
  <div class="row mt-5">
    <div class="col">
		<h2 id="what-is-a-proof-assistant" class="markdown-heading">What is a proof assistant? <a class="hover-link" href="#what-is-a-proof-assistant">#</a></h2>
<p>A <em>proof assistant</em> is a piece of software that provides a language
for defining objects, specifying properties of these objects,
and proving that these specifications hold.
The system checks that these proofs are correct down to their logical foundation.</p>
<p>These tools are often used to verify the correctness of programs.
But they can also be used for abstract mathematics,
which is something of interest to the mathlib community.
In a formalization, all definitions are precisely specified
and all proofs are virtually guaranteed to be correct.</p>

	</div>
  </div>

  <div class="row mt-3">
    <div class="col"> 
	  <h2>Formalized with Lean and mathlib</h2>
	</div>
  </div>
  <div class="row row-cols-1 row-cols-md-2">
	
	  <div class="col mb-4">
		<div class="card" >
		  <div class="card-body">
			  <h5 class="card-title">The cap-set problem</h5>
			<h6 class="card-subtitle mb-2 text-muted">by Dahmen, Hölzl and Lewis</h6>
			<p class="card-text">In 2016, Ellenberg and Gijswijt established a new upper bound on
the size of subsets of $𝔽^n_q$ with no three-term arithmetic
progression. This problem has received much mathematical attention,
particularly in the case $q = 3$, where it is commonly known as the
cap set problem. Ellenberg and Gijswijt's proof was published in
the Annals of Mathematics and is noteworthy for its clever use of
elementary methods.
</p>
		  </div>
          <div class="card-footer text-right bg-white">
            <small><a href="https://lean-forward.github.io/e-g/" class="card-link">Learn more</a></small>
          </div>
		</div>
	  </div>
	
	  <div class="col mb-4">
		<div class="card" >
		  <div class="card-body">
			  <h5 class="card-title">Perfectoid spaces</h5>
			<h6 class="card-subtitle mb-2 text-muted">by Buzzard, Commelin and Massot</h6>
			<p class="card-text">Perfectoid spaces are sophisticated objects in arithmetic
geometry introduced by Peter Scholze in 2012. We formalised enough
definitions and theorems in topology, algebra and geometry to
define perfectoid spaces in the Lean theorem prover. This
experiment confirms that a proof assistant can handle complexity in
that direction, which is rather different from formalising a long
proof about simple objects.
</p>
		  </div>
          <div class="card-footer text-right bg-white">
            <small><a href="https://leanprover-community.github.io/lean-perfectoid-spaces/" class="card-link">Learn more</a></small>
          </div>
		</div>
	  </div>
	
	  <div class="col mb-4">
		<div class="card" >
		  <div class="card-body">
			  <h5 class="card-title">The continuum hypothesis</h5>
			<h6 class="card-subtitle mb-2 text-muted">by Han and van Doorn</h6>
			<p class="card-text">The continuum hypothesis states that there is no cardinality between
the smallest infinite cardinal and the
cardinality of the continuum. It was posed by Cantor in
1878 and was the first problem on Hilbert’s list of twenty-
three unsolved problems in mathematics. Gödel and Cohen proved this
is independent, i.e. neither provable nor disprovable, from ZFC.
</p>
		  </div>
          <div class="card-footer text-right bg-white">
            <small><a href="https://flypitch.github.io/" class="card-link">Learn more</a></small>
          </div>
		</div>
	  </div>
	
	  <div class="col mb-4">
		<div class="card" >
		  <div class="card-body">
			  <h5 class="card-title">Data Types as Quotients of Polynomial Functors</h5>
			<h6 class="card-subtitle mb-2 text-muted">by Avigad, Carneiro and Hudon</h6>
			<p class="card-text">A broad class of data types, including arbitrary nestings of inductive 
types, coinductive types, and quotients, can be represented as quotients 
of polynomial functors. This provides perspicuous ways of constructing 
them and reasoning about them in an interactive theorem prover.
</p>
		  </div>
          <div class="card-footer text-right bg-white">
            <small><a href="https://github.com/avigad/qpf" class="card-link">Learn more</a></small>
          </div>
		</div>
	  </div>
	
  </div>
  <div class="row mt-2 mb-2">
    <div class="col"> 
		You can find many more in the <a href="papers.html">list of papers</a>.
	</div>
  </div>

  
  </div>
</div>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>